p:FinProbSpace, n:, X:RandomVariable(p;n), x:Outcome.
rv-shift(x;X)  RandomVariable(p;n - 1) 

latex

Definitions	t  T, , x:A. B(x), ||as||, P & Q, i  j < k, a < b, P  Q, False, A, A  B, , {x:A| B(x)} , {i..j}, #$n, Void, x:AB(x), l[i], x. t(x), a  j < b. E(j), s = t, type List, , Type, True, n - m, -n, n+m, , T, S  T, cons-seq(x;s), f(a), x.A(x), rv-shift(x;X), RandomVariable(p;n), Outcome, FinProbSpace
Lemmas	cons-seq wf, squash wf, true wf, le wf, nat plus wf, qsum wf, select wf, int seg wf, int inc rationals, length wf1, rationals wf